\begin{tabbing}
change{-}to\=\{i:l\}\+
\\[0ex]($T$; ${\it eq}$; ${\it es}$; $x$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case TERMOF\{change{-}to{-}lemma2:ObjectId, i:l, i:l\}($T$,${\it eq}$,${\it es}$,$x$,$e$)\+
\\[0ex]o\=f inl($p$) =$>$ inl ($p$.1) \+
\\[0ex]$\mid$ inr($q$) =$>$ inr $\cdot$ 
\-\-
\end{tabbing}